COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	first application: the case of alists
C00016 ENDMK
C⊗;
;first application: the case of alists
(wipe-out)
(get-proofs pigeon prf ekl sys)
(proof alpig)

(axiom |∀u.inj(u)⊃disjoint(λm.mkset(nth(u,m)),length u)|)
(label inj_disj)
  
(axiom |∀u v.mklset u=mklset v⊃
             (∀m.m<length u⊃1≤mult(v,mkset nth(u,m)))|)
(label permutp_injectp_lemma)

(axiom |∀u v.mklset u = mklset v ∧
             (∀k.k<length u⊃mult(v,mkset nth(u,k))=1)⊃
             (∀i.i<length v⊃mult(v,mkset nth(v,i))=1)|)
(label mult_mult)

(axiom |∀alist.permutp(alist)⊃injectp(alist)|)
(label theorem_permutp_injectp)
(save-proofs alpig)